\begin{tabbing}
$\forall$\=${\it es}$:ES, $A$:Type, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type,\+
\\[0ex]${\it conds}$:$k$:Knd fp$\rightarrow$ $V$:Type $\times$ (State(${\it ds}$)$\rightarrow$$V$$\rightarrow$($A$ + Top)), $e$:E.
\-\\[0ex]($\forall$$e$:E.
\\[0ex](loc($e$) = $i$)
\\[0ex]$\Rightarrow$ ($\uparrow$kind($e$) $\in$ dom(${\it conds}$))
\\[0ex]$\Rightarrow$ ((valtype($e$) $\subseteq$r (${\it conds}$(kind($e$)).1)) \& (state@loc($e$) $\subseteq$r State(${\it ds}$))))
\\[0ex]$\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ es{-}triggers(${\it es}$;$i$;${\it ds}$;${\it conds}$)))
\\[0ex]$\Rightarrow$ (es{-}triggers(${\it es}$;$i$;${\it ds}$;${\it conds}$)($e$) $\sim$ outl((${\it conds}$(kind($e$)).2)((state when $e$),val($e$))))
\end{tabbing}